import copy
# 列表转字符串
def listtostr(m):
    s = ''
    for i in m:
        s = s + i + ' '
    return s

 # 识别最外层括号，括号位置索引
def braces(m):
    o = []
    p = []
    bralist = []
    for i in range(len(m)):
        if m[i] == '(':
            o.append(-1)
            p.append(i)
            # print('i',i,m[i])
        elif m[i] == ')':
            o.append(1)
            p.append(i)
            # print('i',i,m[i])
        else:
            continue
        t = sum(o)
        if t == 0:
            bralist.append([p[0], p[-1]])
            o = []
            p = []
    # print('最外层括号:',bralist)
    return bralist

# 识别最外层逗号(相继式符号)，返回最外层逗号的位置列表
def comma(m):
    comlist = [-1]  # 为字符串开头加一标志位
    for i in range(len(m)):
        if m[i] == ',' or m[i] == '=>':  # 逗号和相继式符号位置添加到逗号列表
            comlist.append(i)
    return comlist

# 识别符号！和->
def detect(dm):
    dmkuo = braces(dm)
    if dm[0] == '!':
        return 1
    elif dm[1] == '->':
        return 2
    elif dm[1] == '&':
        return 3
    elif dm[1] == '|':
        return 4
    elif dm[1] == '<->':
        return 5
    elif dmkuo!=[]:
     if dm[dmkuo[0][-1] + 1] == '->':
        return 2
     elif dm[dmkuo[0][-1] + 1] == '&':
         return 3
     elif dm[dmkuo[0][-1] + 1] == '|':
         return 4
     elif dm[dmkuo[0][-1] + 1] == '<->':
         return 5

#找出需要处理的字段
def find_(m, comlist):
    # print('find开始：-----------')
    t = m.index('=>')
    if comlist[1] - 1 == comlist[0]:#删除在开头的=>
        comlist.pop(0)
    k = 0
    for i in comlist:
        if i + 2 == len(m) or m[i + 2] == ',' or m[i + 2] == '=>':#长度小于2的单一字段不需要处理
            #  print('单一元素位置：\n',m[i+1:i+2],i+1)
            k = k + 1
            continue
        if comlist[k] == comlist[-1]:#仅剩一个逗号的情况，处理后半段
            last = len(m)
        else:
            last = comlist[k + 1]
        dm = m[i + 1:last]
        print('要处理的子段是：', listtostr(dm))
        dou = last
        j = detect(dm)
        if j == 1:
            if i < t:
                return nonleft(dm, m, dou - 1, i)
            elif i >= t:
                return nonright(dm, m, dou - 1, i)
            break
        elif j == 2:
            if i < t:
                return yunleft(dm, m, dou , i)
            elif i >= t:
                return yunright(dm, m, dou , i)
            break
        elif j == 3:
            return hequ(dm , m , dou , i)
        elif j == 4:
            return xiqu(dm , m , dou , i)
        elif j == 5:
            return dengjia(dm , m , dou , i)
        k = k + 1

# 处理多余逗号
def dd(m):
    for i in range(len(m)):
        if i == len(m) - 1:
            if m[i] == ',':
                m.pop()
            break
        elif m[i] == ',' and m[i + 1] == ',':
            m.pop(i)
        elif m[i] == ',' and m[i + 1] == '=>':
            m.pop(i)
        elif m[i] == '=>' and m[i + 1] == ',':
            m.pop(i+1)
    return m

#i:开始位置 dou:结束位置 ss：要处理的字段
# 按照四种情况处理 M 列表
# 若 a ,!X,b => r  则 a, b =>X,r
def nonleft(ss, m, dou, i):
    ss.pop(0)#删除非
    kuoss = braces(ss)
    if kuoss != []:#删除括号
        ss.pop(0)
        ss.pop(-1)
    for x in range(dou, i, -1):#删除非字段
        m.pop(x)
    m = dd(m)#删除多余逗号
    t = m.index('=>')
    ss.append(",")
    ss.insert(0,"=>")
    m[t:t+1]=ss
    # print('\n"!"在"=>"左边\n', '-------m-------\n',listtostr(m))
    return [[m, '规则1', ' ', [0]]]

# 若 a ,b =>!X, r  则 a, X =>b , r
def nonright(ss, m, dou, i):
    ss.pop(0)#删除非
    kuoss = braces(ss)
    if kuoss != []:#删除括号
        ss.pop(0)
        ss.pop(-1)
    for x in range(dou, i, -1):#删除非字段
        m.pop(x)
    m = dd(m)#删除多余逗号
    t = m.index('=>')
    if t==0:
        ss.append("=>")
        m[t:t+1]=ss
    else:
        ss.insert(0, ",")
        ss.append("=>")
        m[t:t+1]=ss
    # print('\n"!"在"=>"右边\n','-------m-------\n',listtostr(m))
    return [[m, '规则2', ' ', [0]]]

#找出最外层需要处理的->位置
def yunhan(ss):
    dmkuo = braces(ss)
    if ss[1] == '->':
        return 1
    else:
        return dmkuo[0][-1] + 1

# 若 a ,X -> Y,b => r  则 a ,!X,b => r ; a ,Y,b => r
def yunleft(ss, m, dou, i):
    yun = yunhan(ss)
    ssx = ss[:yun]
    ssy = ss[yun + 1:]
    kuossy = braces(ssy)
    if kuossy != []:
        ssy.pop(0)
        ssy.pop(-1)
    ssx.insert(0, '!')
    #m = deal(dou, i)
    m1 = copy.deepcopy(m)
    m2 = copy.deepcopy(m)
    if i==0:
        i=i-1
    m1[i+1:dou]=ssx
    m2[i+1:dou]=ssy
    # print('\n"->"在"=>"左边\n',\
    # '--------m1-------\n',listtostr(m1),\
    # '\n--------m2-------\n',listtostr(m2))
    # return listtostr(m1),listtostr(m2)
    return [[m1, '规则3', ' ', [0]], [m2, '规则3', ' ', [0]]]

# 若 a => b, (X -> Y), r  则 a => b, ！X ， Y , r
def yunright(ss, m, dou, i):
    yun = yunhan(ss)#找出最外层—>位置
    ssx = ss[:yun]
    ssy = ss[yun + 1:]
    kuossy = braces(ssy)
    if kuossy != []:
        ssy.pop(0)
        ssy.pop(-1)
    ssx.insert(0, '!')
    ssxy = ssx + [','] + ssy
    m[i+1:dou]=ssxy
    # print('\n"->"在"=>"右边\n','-------m-------\n',listtostr(m))
    return [[m, '规则4', ' ', [0]]]

#对等价，合取，等价进行转换
#p&q to !(p->!q)   p|q to !p->q   p<->qto !((p->q)->(!(q->p)))
def exchange(m):
 if '&' in m:
   t=m.index("&")
   p=m[0:t]
   q=m[t+1:len(m)]
   return ["!","("]+p+["->"]+q+[")"]
 elif '|' in m:
   t = m.index("|")
   p = m[0:t]
   q = m[t + 1:len(m)]
   return ["!"] + p + ["->"] + q
 elif '<->' in m:
   t = m.index("<->")
   p = m[0:t]
   q = m[t + 1:len(m)]
   return ["!","(","("] + p + ["->"] + q+[")","->","(","!","("]+ p + ["->"] + q+[")",")",")"]

def hequ(ss, m, dou, i):
    ss=exchange(ss)
    m[i + 1:dou]=ss
    return [[m, '合取符号转换', ' ', [0]]]

def xiqu(ss, m, dou, i):
    ss = exchange(ss)
    m[i + 1:dou] = ss
    return [[m, '析取符号转换', ' ', [0]]]

def dengjia(ss, m, dou, i):
    ss = exchange(ss)
    m[i + 1:dou] = ss
    return [[m, '等价符号转换', ' ', [0]]]

if __name__=='__main__':
    s = '=> a -> ( b -> a )'
    s = "=> ( a -> b ) -> ( ( ! b ) -> ( ! a ) )"
    s = '=> ( a -> b ) -> ( ( a -> c ) -> ( a -> ( b & c ) ) )'
    s = '=> ( a -> c ) -> ( ( b -> c ) -> ( ( a | b ) -> c ) )'
    s = '=> ( a <-> b ) -> ( a -> b )'
    # s = input('请输入要推理的字符串(字符之间用空格做间隔)：\n')
    # s = '=>'+' '+s
    m = s.split()
    e = 0
    stock = []
    stock.append([m, '结果', ' ', [0]])
    stock1 = []
    # print('first stock',stock)
    while (stock):
        e = e + 1
        y = 0
        print('\t\t*****', e, '*****')
        mm = stock.pop()
        # print("输出",mm)
        m = mm[0]
        if '->' not in m and '!' not in m and '|' not in m and '&' not in m and '<->' not in m :
            d = m.index('=>')
            m1 = m[:d]
            m2 = m[d + 1:]
            for i in m1:  # 有相同元素，是公理
                if i != ',':
                    if i in m2:
                        print(listtostr(m), '公理', '\n -------END------')
                        stock1.append([listtostr(m), mm[1], '公理', mm[3]])
                        break
                    else:
                        y = y + 1
            for i in m1:
                if i == ',':
                    m1.remove(i)
            if y == len(m1):
                print(listtostr(m), '不是公理', '\n -------END------')
                stock1.append([listtostr(m), mm[1], '不是公理', mm[3]])
                break
            continue
        stock1.append([listtostr(m), mm[1], mm[2], mm[3]])
        print('要处理的字符串:', listtostr(m))
        comlist = comma(m)
        f = find_(m, comlist)
        print('处理后的结果:')
        for i in range(len(f)):  # 规则三返回两个结果
            f[i][3] = [mm[3][0] + i]
            # f[i][3].append(mm[3][i]+i)
            print(listtostr(f[i][0]), f[i][1], '\n -------END------', )
            stock.append(f[i])
    for i in stock1:
        if i[2] == '不是公理':
            print("推理失败!!!\t" + i[0] + i[2])
            exit()
    # 获取规则三的来源
    '''
    for i in stock1:
        print(i)
    '''
    k = []
    for i in range(len(stock1)):
        k.append([len(stock1) - i, stock1[i][3][0]])

    rule3 = []
    for x in range(len(k) - 1):
        if k[x][1] == k[x + 1][1] - 1:
            for i in range(x + 1, len(k)):
                if k[i][1] == k[x][1]:
                    index = i
                    rule3.append([k[x][0], k[index][0], k[x + 1][0]])
                    break
    for i in k:
        print(i)
    print(rule3)
    stock1.reverse()
    print("__________")
    for x in stock1:
     print(x)
    p = []
    for i in range(len(stock1)):
        flag = 1
        for x in rule3:
            if i + 1 == x[0]:
                p.append([stock1[i][0], "由[" + str(x[1]) + "]、[" + str(x[2]) + "]和" + stock1[i - 1][1]])
                flag = 0
        if flag == 1:
            if stock1[i][2] == '公理':
                p.append([stock1[i][0], "公理"])
            else:
                p.append([stock1[i][0], "由[" + str(i) + "]和" + stock1[i - 1][1]])
    print("推理过程：")
    print("_" * 100)
    for i in range(len(p)):
        print("[" + str(i + 1) + "]", "{:<60}".format(p[i][0]), "\t\t", p[i][1])
    print("推理结束")